.title A system to understand incorrect programs
.c
A SYSTEM TO UNDERSTAND INCORRECT PROGRAMS 
.b 5
.c
Harald Wertz 
.b 3
.c
Universite de Paris VIII (Vincennes) 
.c
route de la tourelle 
.c
75571 Paris 
.b 20
.lm 8
.rm 52
Abstract#: 
.br
This paper presents a system (PHENARETE) which understands and improves 
incompletely defined LISP programs, such as those written by students 
beginning to program in LISP. This system takes, as input,  the program 
without any additional information. In order to understand the program, 
the system meta-evaluates it, using a library of "pragmatic rules", 
describing the construction and correction of general program constructs, 
and a set of "specialists", describing the syntax and semantics of the 
standard LISP functions.  The system can use its understanding of the 
program to detect errors in it,  to debug them and, eventually, to 
justify its proposed modifications. 
This paper gives a brief survey of the working of the system, 
emphasizing on some commented examples. 
.page
.lm 0
.rm 62
A lot of effort is actually spent on the developpement of tools to help 
programmers in constructing, debugging and verifying programs. 
Unfortunately  most of these tools 
.br
- impose too  much constraints on the 
intuitions of the programmer [cf DIJKSTRA 1976], 
.br
- are working only 
on  a very limited subset of possible programs [cf RUTH 1974],
.br
- are only 
working on correct programs [cf ARSAC 1977, IGARASHI et al 1975]. 
.b 1
Our aim is two-fold#: 
.lm 8
.p -4,1,1
   -1- to make explicit the knowledge involved in constructing and debugging 
       programs and 
.p -4,1,1
   -2- to verify - not the correctness of programs - but their "consistency" 
       and to provide "hints" for improving and correcting their programs 
       to the programmer.
.lm 0
.b 2
To this end we have build our system on four main concepts#:    
 1 an algorithm of meta-evaluation [cf GOOSSENS 1978]   
to help the system to understand  
   each of the possible paths of the program, 
.br
 2 a set of "specialists", i.e. a set of procedural specifications 
   of the syntax and the operational semantics of the standard  
   LISP functions,  
.b 
   example#: specialist CAR for the syntax  
.b   
.nofill 
   [CAR-1 (X) =>   
           v (←& atom (CAR X) 
              ←& type (X) = LISTP) 
           v (←& S-expression (CAR X) 
    	      ←& type (val (X)) = LISTP)  
     else#: 
              modify X until CAR-1 (X) = T]  
.fill 
.b 2 
paraphrasing#: 
.b
.rm 45
.lm 3 
CAR expects that its argument is 
.lm 7 
- an atom 
.lm 9    
.br
and the type of the value of the argument is a list 
.lm 7.br   
- a S-expression 
.lm 9   
.br
and the type of the value of that S-expression is a list 
.br   
.lm 5 
else 
.br    
.lm 9 
CAR has to modify the argument until one of these two conditions is true 
.b 2 
.lm 0    
.rm 62 
and the specialist CAR for the semantics 
.b 
.tp 8
.nofill 
    [CAR-N =>  
         arg#: (X (meta-eval X)) 
        test#: (type (val (X)) = LISTP) -> 
               (type (val (X)) = ?) 
		      -> hypothesize (X, type#LISTP) 
     	       T -> complain (X, type#: LISTP) 
      action#: if (existe (CAR X)) --> (CAR X) 
               else (create (CAR, X)) --> (CAR X)] 
.fill 
.b 2 
or in paraphrasing#: 
.rm 55
.b
.lm 4 
CAR-N 
.b  
.lm 7 
has an argument named X, which must   be evaluated   
.br
one must verify   
.br 
.lm 9 
if 
.lm 12
  the type of value of the argument is a list, all is ok   
.lm 9
else 
.lm 12
if the type of value of the argument isn't known, one has to 
create a hypothetical value of type LIST for X 
.lm 9 
else    
.lm 12
one has to ask the debugger to change the text of the program 
in such a way that the value of X becomes a list 
.b
.lm 7 
the value of CAR is 
.br
.lm 9 
if 
.lm 12
there exists already a CAR of X, this CAR 
.lm 9
.br
else 
.lm 12
one has to create a symbolic value for X, the CAR of which 
will be the desired value 
.lm 0 
.rm 62 
.b 2
These specialists are the agents of the meta-evaluation and 
they represent the system's knowledge about the programming 
language used.
.b
3 a set of "pragmatic rules" describing general program constructs and 
methods to repair inconsistencies
.b
example#:  
.br
.lm 5
.rm 55 
rule of the dependence of a loop of the predicate#=> 
.b
if no variable of the exit-test is modified inside the loop,
then the loop is independent of the exit-test  and,          
its execution is non-terminating or the loop will never be 
executed.       
.b
.lm 0
.rm 62
The set of these rules expresses the system's general knowledge  
about the well-formedness of programs and about the correction of errors;
.b
4 during the analysis of a program, PHENARETE contructs some description 
-#an internal representation#- of the program under the form of 
"cognitive atoms". These may be considered as the nodes of a  
network-like representation of the program actually analysed.
.b 2 
The system accepts every LISP program conforming to the following 
restrictions#: 
.br
.lm 5
.p -2,1,1
- partitioning of the names of variables, funtions and labels;
.p -2,1,1
- all funtion calls must be  "call by name";
.p -2,1,1
- the unique functional arguments admitted are explicit lambda-expressions.
.b 
.lm 0 
We call this subset of LISP#:  extended first order LISP.
.b 2   
To use  PHENARETE,  the user has to  give to the system only  
the text of the draft version of the program he wants to write, 
without any additional information like input/output assertions,
commentaries, plans etc. The system will try to understand what the 
user  wanted to do, and, if necessary, modify                          
                the text of the programm.   
.b 2
To give some feeling of the working of the system, let us examine 
some examples in detail#:
.br
Our first example is a (very) erroneous version of the well known 
REVERSE function. Here is the actual input to the system#:
.b   
.nofill 
?  (P '(DE REV L1 L2 COND ULL L22 A1 T RVE A1 ONS CRA A1 A2))
.fill
.b
PHENARETE will first 
correct the spelling errors#:
.b
.nofill
   ERREUR: 
              NOM --> (? ULL --> NULL)
   ERREUR: 
              NOM --> (? L22 --> L2)
   ERREUR: 
              NOM --> (? A1 --> L1)
   ERREUR: 
              NOM --> (? A1 --> L1)
   ERREUR: 
              NOM --> (? RVE --> REV)
   ERREUR: 
              NOM --> (? RVE --> REV)
   ERREUR: 
              NOM --> (? A1 --> L1)
   ERREUR: 
              NOM --> (? ONS --> CONS)
   ERREUR: 
              NOM --> (? CRA --> CAR)
   ERREUR: 
              NOM --> (? A1 --> L1)
   ERREUR: 
              NOM --> (? A2 --> L2)
 
.fill
.b
After having very well corrected the spelling errors, PHENARETE  
proceeds to a first analysis where she uses only her syntactic 
knowledge. The result of this first analysis is a "syntactically 
correct" LISP program (i.e. a programm accepted by any smart     
LISP interpreter or compiler)#: 
.b   
.tp 7
.nofill
   PROPOSITION 1 : 
  
   (DE REV (L1 L2) 
      (COND
         ((NULL L2) L1)
         (T (REV L1 (CONS (CAR L1) L2)))))
.fill
.b
These first improvements have eliminated all the syntactic errors.
Anyway, there subsist two    semantic errors#:  
.lm 5
.p -3,1,1 
-1  in the recursive call of rev, the first argument L1 is not 
modified. This creates an infinit recursion.
.p -3,1,1
-2  even with a modification of L1 in the recursive call, the 
recursion won't stop either since the stop-test has as argument L2, 
a list which grows longer and longer in the run of the succesive 
recursive calls.
.b
.lm 0
PHENARETE can not disambiguate this function -#she does not know 
anything of the intentions of the programmer#- so she gives two 
different propositions#: 
.b
.nofill 
PROPOSITION 2 : 
            
   (DE REV (L1 L2) 
      (COND
         ((NULL L2) L1)
         ((NULL L1) L2)
         (T (REV (CDR L1) (CONS (CAR L1) L2)))))
            
              AT LEAST YOUR FUNCTION SEEMS OK TO ME.
            
.fill 
In this first proposition, PHENARETE supposed the stop-test given 
to be true, but that the user omitted a second stop-test for the case 
where the second argument is not NULL at the initial call of REV. 
.b 
.tp 8
.nofill
            
   P R O P O S I T I O N :
  
   (DE REV (L1 L2) 
      (COND
         ((NULL L1) L2)
         (T (REV (CDR L1) (CONS (CAR L1) L2)))))
   
              AT LEAST YOUR FUNCTION SEEMS OK TO ME.
.fill 
.b
In this second proposition, PHENARETE supposed that the user 
inadvertently inverted the  arguments of the stop-test, so 
she inverts the two arguments L1 and L2.
.br
Of the two corrected versions of the initial draft-program 
PHENARETE is assured that they will stop and deliver a result when    
running.       
.b 2
Our second example is an extremly "simplified" version of 
the equally well known function FACTORIAL. Here she is#:
.b
.nofill         
?  (DE FACT N TIMES N FACT N)
.fill
.b
As in the previous example, PHENARETE will first translate this 
unparentesized expression into an well parentesized one#:        
.b
.nofill
   PROPOSITION 1 : 
  
   (DE FACT (N) (TIMES N (FACT N)))
.fill
.b
This first proposition is a syntactically correct program, but 
semantically it is not very correct#:
.lm 5
.b
.p -2,1,1
-1 at the recursive call N is not modified. This is  
the same kind of error as in the previous example, exept the   
argument here is of numeric type.
.p -2,1,1
-2 there is no stop-test at all, so there are two (!) reasons 
to make the recursion infinit.
.lm 0
.b  
Remember that PHENARETE doesn't know the intentions of the 
programmer, so she must detect these errors without any 
additional information#: all she can use in the further analysis
are the semantic specialists and the pragmatic rules. So let us look 
at her proposition#: 
.b                 
.nofill 
  P R O P O S I T I O N :
  
   (DE FACT (N) (COND
      ((LE N 0) 1)
      (T (TIMES N (FACT (SUB1 N))))))
   
              AT LEAST YOUR FUNCTION SEEMS OK TO ME.
.fill
.b
This corrected version is actually a correct version of the 
factorial-program. The performance is  really astonishing 
knowing that the system works completely automatically whithout 
asking any question to the user and without any information about 
the supposed intention. 
.b2
One last (uncommented) example#:
.b
.nofill               
?  (DE ADDIT M N  ((ZEROP N) M)    
                  (T (ADDIT SUB1 M ADD1 N)))
   
   PROPOSITION 1 : 
  
  (DE ADDIT (M N) 
      (COND
         ((ZEROP N) M)
         (T (ADDIT (SUB1 M) (ADD1 N)))))
  
  
   P R O P O S I T I O N :
  (DE ADDIT (M N) 
      (COND
         ((ZEROP N) M)
         ((LE M 0) N)
         (T (ADDIT (SUB1 M) (ADD1 N)))))
   
              AT LEAST YOUR FUNCTION SEEMS OK TO ME.
     
.fill  
.b 2 
Presently we are working on some extensions as to find automatically 
the intentions and the goals of given pieces of code. We would also 
like to adjoin to PHENARETE a module permitting to explain the reasoning 
of the system. This would be a  great help to the user. 
.br
The system is running on PDP-10, uses about 25k word memory, is implemented 
in VLISP [CHAILLOUX 1976, GREUSSAY 1977], and is used by about 
1000 students in our university.  
.br 
A more detailed description may be found in [WERTZ 1978].

.page
.c 
references
.b
.lm 10
.p -10,1,1
ARSAC J., (1977), La construction de programmes structures, 
Dunod-Informatique, Paris 
.p -10,1,1
CHAILLOUX J., (1976), VLISP-10 manuel de reference, 
Dept. Informatique, Universite Paris 8, RT-17-76    
.p -10,1,1
DIJKSTRA E.W., (1976), A Discipline of Programming, 
Prentice-Hall, Inc., Englewood Cliffs, N.J. 
.p -10,1,1
GOOSSENS D., (1978), A System For Visual-Like Understanding of 
LISP Programs, Proc. AISB/GI Conference, Hamburg, RFA,  
july 17-19, 1978  
.p -10,1,1
GREUSSAY P., (1977), Contribution a la Definition 
Interpretative 
et a l'Implementation des Lambda-langages, These, Universite Paris#7.
.p -10,1,1
IGARASHI S., LONDON R.L. ←& LUCKHAM D.C., (1975), Automatic 
Program 
Verification 1#: Logical Basis and its Implementation, Acta Informatica, 
vol. 4, pp. 145-182.
.p -10,1,1
RUTH G.R., (1974), Analysis of Algorithm Implementations, 
M.I.T., MAC-TR-130. 
.p -10,1,1
WERTZ H., (1978), Un systeme de comprehension, d'amelioration 
et de correction de programmes incorrects, These de 3eme cycle, 
Universite Paris 6